|
In computer science, symbolic execution (also symbolic evaluation) is a means of analyzing a program to determine what inputs cause each part of a program to execute. An interpreter follows the program, assuming symbolic values for inputs rather than obtaining actual inputs as normal execution of the program would, a case of abstract interpretation. It thus arrives at expressions in terms of those symbols for expressions and variables in the program, and constraints in terms of those symbols for the possible outcomes of each conditional branch. The field of symbolic simulation applies the same concept to hardware. Symbolic computation applies the concept to the analysis of mathematical expressions. ==Example== Consider the program below, which reads in a value and fails if the input is 6. y = read() y = 2 * y if (y == 12) fail() print("OK") When a program analyzer symbolically executes this program, it does not have a concrete number for the input value — the result of read() — so assigns the symbol 's' to it. The statement "y = read()" thus assigns the value 's' to program variable y. Then the statement "y = 2 * y" assigns the value '2 * s' to y. The next statement has two possible control flows: the true branch and the false branch. Which gets taken when the program executes for real depends upon the input value ('s'). The analyzer associates the constraint '2 * s == 12' with the true branch, which means it recognizes that the "fail()" statement executes in real execution if and only if '2 * s == 12' is true. The constraint "2 * s == 12 is true" is known as a path constraint. Assume the goal of the analysis is to determine what inputs cause the "fail()" statement to execute. The analyzer uses a constraint solver to determine what values of 's' make '2 * s == 12' true, and thus determines that '6' is the answer. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Symbolic execution」の詳細全文を読む スポンサード リンク
|